Far beyond Goodman's Theorem?

Abstract: Goodman's Theorem says that Heyting arithmetic in all finite types, HA^{\omega}, augmented by the axiom of choice for all finite types, AC(FT), is conservative over HA. This classical result has been extended to many other intuitionistic theories (e.g. by Beeson) and even to intuitionistic Zermelo-Fraenkel set theory with large set axioms (by Friedman and Scedrov).The question I'll be pondering in this talk is whether the finite types are the limit.What about adding the axiom of choice for all the transfinite dependent types as they appear in Martin-Löf type theory (actually already in Hilbert's "Über das Unendliche")?

logic in computer sciencelogic

Audience: researchers in the topic

Proof Theory Virtual Seminar

Series comments: The Proof Theory Virtual Seminar presents talks by leading researchers from all areas of proof theory. Everyone who is interested in the subject is warmly invited to attend! In order to participate, please visit the seminar webpage: www.proofsociety.org/proof-theory-seminar/